Termination w.r.t. Q proof of /tmp/tmpin0wRC/dup12.srs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

b(b(d(d(b(b(x1)))))) → c(c(d(d(b(b(x1))))))
b(b(a(a(c(c(x1)))))) → b(b(c(c(x1))))
a(a(d(d(x1)))) → d(d(c(c(x1))))
b(b(b(b(b(b(x1)))))) → a(a(b(b(c(c(x1))))))
d(d(c(c(x1)))) → b(b(d(d(x1))))
d(d(c(c(x1)))) → d(d(b(b(d(d(x1))))))
d(d(a(a(c(c(x1)))))) → b(b(b(b(x1))))

Q is empty.

↳ QTRS

  ↳ QTRS Reverse

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

b(b(d(d(b(b(x1)))))) → c(c(d(d(b(b(x1))))))
b(b(a(a(c(c(x1)))))) → b(b(c(c(x1))))
a(a(d(d(x1)))) → d(d(c(c(x1))))
b(b(b(b(b(b(x1)))))) → a(a(b(b(c(c(x1))))))
d(d(c(c(x1)))) → b(b(d(d(x1))))
d(d(c(c(x1)))) → d(d(b(b(d(d(x1))))))
d(d(a(a(c(c(x1)))))) → b(b(b(b(x1))))

Q is empty.

We have reversed the following QTRS:
The set of rules R is

b(b(d(d(b(b(x1)))))) → c(c(d(d(b(b(x1))))))
b(b(a(a(c(c(x1)))))) → b(b(c(c(x1))))
a(a(d(d(x1)))) → d(d(c(c(x1))))
b(b(b(b(b(b(x1)))))) → a(a(b(b(c(c(x1))))))
d(d(c(c(x1)))) → b(b(d(d(x1))))
d(d(c(c(x1)))) → d(d(b(b(d(d(x1))))))
d(d(a(a(c(c(x1)))))) → b(b(b(b(x1))))

The set Q is empty.
We have obtained the following QTRS:

b(b(d(d(b(b(x)))))) → b(b(d(d(c(c(x))))))
c(c(a(a(b(b(x)))))) → c(c(b(b(x))))
d(d(a(a(x)))) → c(c(d(d(x))))
b(b(b(b(b(b(x)))))) → c(c(b(b(a(a(x))))))
c(c(d(d(x)))) → d(d(b(b(x))))
c(c(d(d(x)))) → d(d(b(b(d(d(x))))))
c(c(a(a(d(d(x)))))) → b(b(b(b(x))))

The set Q is empty.

↳ QTRS

  ↳ QTRS Reverse

    ↳ QTRS

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

b(b(d(d(b(b(x)))))) → b(b(d(d(c(c(x))))))
c(c(a(a(b(b(x)))))) → c(c(b(b(x))))
d(d(a(a(x)))) → c(c(d(d(x))))
b(b(b(b(b(b(x)))))) → c(c(b(b(a(a(x))))))
c(c(d(d(x)))) → d(d(b(b(x))))
c(c(d(d(x)))) → d(d(b(b(d(d(x))))))
c(c(a(a(d(d(x)))))) → b(b(b(b(x))))

Q is empty.

We have reversed the following QTRS:
The set of rules R is

b(b(d(d(b(b(x1)))))) → c(c(d(d(b(b(x1))))))
b(b(a(a(c(c(x1)))))) → b(b(c(c(x1))))
a(a(d(d(x1)))) → d(d(c(c(x1))))
b(b(b(b(b(b(x1)))))) → a(a(b(b(c(c(x1))))))
d(d(c(c(x1)))) → b(b(d(d(x1))))
d(d(c(c(x1)))) → d(d(b(b(d(d(x1))))))
d(d(a(a(c(c(x1)))))) → b(b(b(b(x1))))

The set Q is empty.
We have obtained the following QTRS:

b(b(d(d(b(b(x)))))) → b(b(d(d(c(c(x))))))
c(c(a(a(b(b(x)))))) → c(c(b(b(x))))
d(d(a(a(x)))) → c(c(d(d(x))))
b(b(b(b(b(b(x)))))) → c(c(b(b(a(a(x))))))
c(c(d(d(x)))) → d(d(b(b(x))))
c(c(d(d(x)))) → d(d(b(b(d(d(x))))))
c(c(a(a(d(d(x)))))) → b(b(b(b(x))))

The set Q is empty.

↳ QTRS

  ↳ QTRS Reverse

  ↳ QTRS Reverse

    ↳ QTRS

  ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

b(b(d(d(b(b(x)))))) → b(b(d(d(c(c(x))))))
c(c(a(a(b(b(x)))))) → c(c(b(b(x))))
d(d(a(a(x)))) → c(c(d(d(x))))
b(b(b(b(b(b(x)))))) → c(c(b(b(a(a(x))))))
c(c(d(d(x)))) → d(d(b(b(x))))
c(c(d(d(x)))) → d(d(b(b(d(d(x))))))
c(c(a(a(d(d(x)))))) → b(b(b(b(x))))

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

b(b(d(d(b(b(x1)))))) → c(c(d(d(b(b(x1))))))
b(b(a(a(c(c(x1)))))) → b(b(c(c(x1))))
a(a(d(d(x1)))) → d(d(c(c(x1))))
b(b(b(b(b(b(x1)))))) → a(a(b(b(c(c(x1))))))
d(d(c(c(x1)))) → b(b(d(d(x1))))
d(d(c(c(x1)))) → d(d(b(b(d(d(x1))))))
d(d(a(a(c(c(x1)))))) → b(b(b(b(x1))))

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

b(b(a(a(c(c(x1)))))) → b(b(c(c(x1))))

Used ordering:
Polynomial interpretation [25]:

POL(a(x₁)) = 2 + 2·x₁
POL(b(x₁)) = 2 + 2·x₁
POL(c(x₁)) = 2 + 2·x₁
POL(d(x₁)) = x₁

↳ QTRS

  ↳ QTRS Reverse

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

b(b(d(d(b(b(x1)))))) → c(c(d(d(b(b(x1))))))
a(a(d(d(x1)))) → d(d(c(c(x1))))
b(b(b(b(b(b(x1)))))) → a(a(b(b(c(c(x1))))))
d(d(c(c(x1)))) → b(b(d(d(x1))))
d(d(c(c(x1)))) → d(d(b(b(d(d(x1))))))
d(d(a(a(c(c(x1)))))) → b(b(b(b(x1))))

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

B(b(b(b(b(b(x1)))))) → A(a(b(b(c(c(x1))))))
D(d(a(a(c(c(x1)))))) → B(b(b(b(x1))))
A(a(d(d(x1)))) → D(c(c(x1)))
D(d(a(a(c(c(x1)))))) → B(b(b(x1)))
D(d(a(a(c(c(x1)))))) → B(b(x1))
D(d(c(c(x1)))) → D(b(b(d(d(x1)))))
D(d(a(a(c(c(x1)))))) → B(x1)
B(b(b(b(b(b(x1)))))) → A(b(b(c(c(x1)))))
D(d(c(c(x1)))) → D(d(x1))
B(b(b(b(b(b(x1)))))) → B(b(c(c(x1))))
B(b(b(b(b(b(x1)))))) → B(c(c(x1)))
D(d(c(c(x1)))) → B(d(d(x1)))
A(a(d(d(x1)))) → D(d(c(c(x1))))
D(d(c(c(x1)))) → B(b(d(d(x1))))
D(d(c(c(x1)))) → D(d(b(b(d(d(x1))))))
D(d(c(c(x1)))) → D(x1)

The TRS R consists of the following rules:

b(b(d(d(b(b(x1)))))) → c(c(d(d(b(b(x1))))))
a(a(d(d(x1)))) → d(d(c(c(x1))))
b(b(b(b(b(b(x1)))))) → a(a(b(b(c(c(x1))))))
d(d(c(c(x1)))) → b(b(d(d(x1))))
d(d(c(c(x1)))) → d(d(b(b(d(d(x1))))))
d(d(a(a(c(c(x1)))))) → b(b(b(b(x1))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ QTRS Reverse

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

B(b(b(b(b(b(x1)))))) → A(a(b(b(c(c(x1))))))
D(d(a(a(c(c(x1)))))) → B(b(b(b(x1))))
A(a(d(d(x1)))) → D(c(c(x1)))
D(d(a(a(c(c(x1)))))) → B(b(b(x1)))
D(d(a(a(c(c(x1)))))) → B(b(x1))
D(d(c(c(x1)))) → D(b(b(d(d(x1)))))
D(d(a(a(c(c(x1)))))) → B(x1)
B(b(b(b(b(b(x1)))))) → A(b(b(c(c(x1)))))
D(d(c(c(x1)))) → D(d(x1))
B(b(b(b(b(b(x1)))))) → B(b(c(c(x1))))
B(b(b(b(b(b(x1)))))) → B(c(c(x1)))
D(d(c(c(x1)))) → B(d(d(x1)))
A(a(d(d(x1)))) → D(d(c(c(x1))))
D(d(c(c(x1)))) → B(b(d(d(x1))))
D(d(c(c(x1)))) → D(d(b(b(d(d(x1))))))
D(d(c(c(x1)))) → D(x1)

The TRS R consists of the following rules:

b(b(d(d(b(b(x1)))))) → c(c(d(d(b(b(x1))))))
a(a(d(d(x1)))) → d(d(c(c(x1))))
b(b(b(b(b(b(x1)))))) → a(a(b(b(c(c(x1))))))
d(d(c(c(x1)))) → b(b(d(d(x1))))
d(d(c(c(x1)))) → d(d(b(b(d(d(x1))))))
d(d(a(a(c(c(x1)))))) → b(b(b(b(x1))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 12 less nodes.

↳ QTRS

  ↳ QTRS Reverse

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

              ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

D(d(c(c(x1)))) → D(d(x1))
D(d(c(c(x1)))) → D(b(b(d(d(x1)))))
D(d(c(c(x1)))) → D(d(b(b(d(d(x1))))))
D(d(c(c(x1)))) → D(x1)

The TRS R consists of the following rules:

b(b(d(d(b(b(x1)))))) → c(c(d(d(b(b(x1))))))
a(a(d(d(x1)))) → d(d(c(c(x1))))
b(b(b(b(b(b(x1)))))) → a(a(b(b(c(c(x1))))))
d(d(c(c(x1)))) → b(b(d(d(x1))))
d(d(c(c(x1)))) → d(d(b(b(d(d(x1))))))
d(d(a(a(c(c(x1)))))) → b(b(b(b(x1))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS

  ↳ QTRS Reverse

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

                ↳ QDP

                  ↳ RuleRemovalProof

              ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

D(d(c(c(x1)))) → D(d(x1))
D(d(c(c(x1)))) → D(b(b(d(d(x1)))))
D(d(c(c(x1)))) → D(d(b(b(d(d(x1))))))
D(d(c(c(x1)))) → D(x1)

The TRS R consists of the following rules:

d(d(c(c(x1)))) → b(b(d(d(x1))))
d(d(c(c(x1)))) → d(d(b(b(d(d(x1))))))
d(d(a(a(c(c(x1)))))) → b(b(b(b(x1))))
b(b(d(d(b(b(x1)))))) → c(c(d(d(b(b(x1))))))
b(b(b(b(b(b(x1)))))) → a(a(b(b(c(c(x1))))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

D(d(c(c(x1)))) → D(d(x1))
D(d(c(c(x1)))) → D(x1)

Used ordering: POLO with Polynomial interpretation [25]:

POL(D(x₁)) = x₁
POL(a(x₁)) = 1 + 2·x₁
POL(b(x₁)) = 1 + 2·x₁
POL(c(x₁)) = 1 + 2·x₁
POL(d(x₁)) = x₁

↳ QTRS

  ↳ QTRS Reverse

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

                ↳ QDP

                  ↳ RuleRemovalProof

                    ↳ QDP

                      ↳ QDPOrderProof

              ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

D(d(c(c(x1)))) → D(b(b(d(d(x1)))))
D(d(c(c(x1)))) → D(d(b(b(d(d(x1))))))

The TRS R consists of the following rules:

d(d(c(c(x1)))) → b(b(d(d(x1))))
d(d(c(c(x1)))) → d(d(b(b(d(d(x1))))))
d(d(a(a(c(c(x1)))))) → b(b(b(b(x1))))
b(b(d(d(b(b(x1)))))) → c(c(d(d(b(b(x1))))))
b(b(b(b(b(b(x1)))))) → a(a(b(b(c(c(x1))))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

D(d(c(c(x1)))) → D(b(b(d(d(x1)))))

The remaining pairs can at least be oriented weakly.

D(d(c(c(x1)))) → D(d(b(b(d(d(x1))))))

Used ordering: Polynomial Order [21,25] with Interpretation:

POL( c(x₁) ) = max{0, -1}

POL( d(x₁) ) = 1

POL( b(x₁) ) = max{0, -1}

POL( D(x₁) ) = x₁ + 1

POL( a(x₁) ) = max{0, -1}

The following usable rules [17] were oriented:

d(d(a(a(c(c(x1)))))) → b(b(b(b(x1))))
b(b(d(d(b(b(x1)))))) → c(c(d(d(b(b(x1))))))
d(d(c(c(x1)))) → b(b(d(d(x1))))
d(d(c(c(x1)))) → d(d(b(b(d(d(x1))))))
b(b(b(b(b(b(x1)))))) → a(a(b(b(c(c(x1))))))

↳ QTRS

  ↳ QTRS Reverse

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

                ↳ QDP

                  ↳ RuleRemovalProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ Narrowing

              ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

D(d(c(c(x1)))) → D(d(b(b(d(d(x1))))))

The TRS R consists of the following rules:

d(d(c(c(x1)))) → b(b(d(d(x1))))
d(d(c(c(x1)))) → d(d(b(b(d(d(x1))))))
d(d(a(a(c(c(x1)))))) → b(b(b(b(x1))))
b(b(d(d(b(b(x1)))))) → c(c(d(d(b(b(x1))))))
b(b(b(b(b(b(x1)))))) → a(a(b(b(c(c(x1))))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule D(d(c(c(x1)))) → D(d(b(b(d(d(x1)))))) at position [0] we obtained the following new rules:

D(d(c(c(d(c(c(x0))))))) → D(d(b(b(d(b(b(d(d(x0)))))))))
D(d(c(c(d(c(c(x0))))))) → D(d(b(b(d(d(d(b(b(d(d(x0)))))))))))
D(d(c(c(b(b(x0)))))) → D(d(c(c(d(d(b(b(x0))))))))
D(d(c(c(a(a(c(c(x0)))))))) → D(d(b(b(b(b(b(b(x0))))))))
D(d(c(c(d(a(a(c(c(x0))))))))) → D(d(b(b(d(b(b(b(b(x0)))))))))
D(d(c(c(c(c(x0)))))) → D(d(b(b(d(d(b(b(d(d(x0))))))))))
D(d(c(c(c(c(x0)))))) → D(d(b(b(b(b(d(d(x0))))))))

↳ QTRS

  ↳ QTRS Reverse

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

                ↳ QDP

                  ↳ RuleRemovalProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ Narrowing

              ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

D(d(c(c(d(c(c(x0))))))) → D(d(b(b(d(b(b(d(d(x0)))))))))
D(d(c(c(d(c(c(x0))))))) → D(d(b(b(d(d(d(b(b(d(d(x0)))))))))))
D(d(c(c(b(b(x0)))))) → D(d(c(c(d(d(b(b(x0))))))))
D(d(c(c(d(a(a(c(c(x0))))))))) → D(d(b(b(d(b(b(b(b(x0)))))))))
D(d(c(c(a(a(c(c(x0)))))))) → D(d(b(b(b(b(b(b(x0))))))))
D(d(c(c(c(c(x0)))))) → D(d(b(b(d(d(b(b(d(d(x0))))))))))
D(d(c(c(c(c(x0)))))) → D(d(b(b(b(b(d(d(x0))))))))

The TRS R consists of the following rules:

d(d(c(c(x1)))) → b(b(d(d(x1))))
d(d(c(c(x1)))) → d(d(b(b(d(d(x1))))))
d(d(a(a(c(c(x1)))))) → b(b(b(b(x1))))
b(b(d(d(b(b(x1)))))) → c(c(d(d(b(b(x1))))))
b(b(b(b(b(b(x1)))))) → a(a(b(b(c(c(x1))))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule D(d(c(c(a(a(c(c(x0)))))))) → D(d(b(b(b(b(b(b(x0)))))))) at position [0] we obtained the following new rules:

D(d(c(c(a(a(c(c(b(b(b(b(b(x0))))))))))))) → D(d(b(b(b(b(b(a(a(b(b(c(c(x0)))))))))))))
D(d(c(c(a(a(c(c(b(b(b(x0))))))))))) → D(d(b(b(b(a(a(b(b(c(c(x0)))))))))))
D(d(c(c(a(a(c(c(b(d(d(b(b(x0))))))))))))) → D(d(b(b(b(b(b(c(c(d(d(b(b(x0)))))))))))))
D(d(c(c(a(a(c(c(b(x0))))))))) → D(d(b(a(a(b(b(c(c(x0)))))))))
D(d(c(c(a(a(c(c(b(b(b(b(x0)))))))))))) → D(d(b(b(b(b(a(a(b(b(c(c(x0))))))))))))
D(d(c(c(a(a(c(c(d(d(b(b(x0)))))))))))) → D(d(b(b(b(b(c(c(d(d(b(b(x0))))))))))))
D(d(c(c(a(a(c(c(x0)))))))) → D(d(a(a(b(b(c(c(x0))))))))
D(d(c(c(a(a(c(c(b(b(x0)))))))))) → D(d(b(b(a(a(b(b(c(c(x0))))))))))

↳ QTRS

  ↳ QTRS Reverse

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

                ↳ QDP

                  ↳ RuleRemovalProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ DependencyGraphProof

              ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

D(d(c(c(a(a(c(c(b(b(b(x0))))))))))) → D(d(b(b(b(a(a(b(b(c(c(x0)))))))))))
D(d(c(c(a(a(c(c(b(d(d(b(b(x0))))))))))))) → D(d(b(b(b(b(b(c(c(d(d(b(b(x0)))))))))))))
D(d(c(c(d(c(c(x0))))))) → D(d(b(b(d(d(d(b(b(d(d(x0)))))))))))
D(d(c(c(a(a(c(c(b(x0))))))))) → D(d(b(a(a(b(b(c(c(x0)))))))))
D(d(c(c(b(b(x0)))))) → D(d(c(c(d(d(b(b(x0))))))))
D(d(c(c(a(a(c(c(x0)))))))) → D(d(a(a(b(b(c(c(x0))))))))
D(d(c(c(c(c(x0)))))) → D(d(b(b(d(d(b(b(d(d(x0))))))))))
D(d(c(c(d(c(c(x0))))))) → D(d(b(b(d(b(b(d(d(x0)))))))))
D(d(c(c(a(a(c(c(b(b(b(b(b(x0))))))))))))) → D(d(b(b(b(b(b(a(a(b(b(c(c(x0)))))))))))))
D(d(c(c(a(a(c(c(b(b(b(b(x0)))))))))))) → D(d(b(b(b(b(a(a(b(b(c(c(x0))))))))))))
D(d(c(c(d(a(a(c(c(x0))))))))) → D(d(b(b(d(b(b(b(b(x0)))))))))
D(d(c(c(a(a(c(c(d(d(b(b(x0)))))))))))) → D(d(b(b(b(b(c(c(d(d(b(b(x0))))))))))))
D(d(c(c(a(a(c(c(b(b(x0)))))))))) → D(d(b(b(a(a(b(b(c(c(x0))))))))))
D(d(c(c(c(c(x0)))))) → D(d(b(b(b(b(d(d(x0))))))))

The TRS R consists of the following rules:

d(d(c(c(x1)))) → b(b(d(d(x1))))
d(d(c(c(x1)))) → d(d(b(b(d(d(x1))))))
d(d(a(a(c(c(x1)))))) → b(b(b(b(x1))))
b(b(d(d(b(b(x1)))))) → c(c(d(d(b(b(x1))))))
b(b(b(b(b(b(x1)))))) → a(a(b(b(c(c(x1))))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 8 less nodes.

↳ QTRS

  ↳ QTRS Reverse

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

                ↳ QDP

                  ↳ RuleRemovalProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ QDP

                                      ↳ Narrowing

              ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

D(d(c(c(d(c(c(x0))))))) → D(d(b(b(d(b(b(d(d(x0)))))))))
D(d(c(c(d(c(c(x0))))))) → D(d(b(b(d(d(d(b(b(d(d(x0)))))))))))
D(d(c(c(b(b(x0)))))) → D(d(c(c(d(d(b(b(x0))))))))
D(d(c(c(d(a(a(c(c(x0))))))))) → D(d(b(b(d(b(b(b(b(x0)))))))))
D(d(c(c(c(c(x0)))))) → D(d(b(b(d(d(b(b(d(d(x0))))))))))
D(d(c(c(c(c(x0)))))) → D(d(b(b(b(b(d(d(x0))))))))

The TRS R consists of the following rules:

d(d(c(c(x1)))) → b(b(d(d(x1))))
d(d(c(c(x1)))) → d(d(b(b(d(d(x1))))))
d(d(a(a(c(c(x1)))))) → b(b(b(b(x1))))
b(b(d(d(b(b(x1)))))) → c(c(d(d(b(b(x1))))))
b(b(b(b(b(b(x1)))))) → a(a(b(b(c(c(x1))))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule D(d(c(c(d(a(a(c(c(x0))))))))) → D(d(b(b(d(b(b(b(b(x0))))))))) at position [0] we obtained the following new rules:

D(d(c(c(d(a(a(c(c(b(b(x0))))))))))) → D(d(b(b(d(a(a(b(b(c(c(x0)))))))))))
D(d(c(c(d(a(a(c(c(b(d(d(b(b(x0)))))))))))))) → D(d(b(b(d(b(b(b(c(c(d(d(b(b(x0))))))))))))))
D(d(c(c(d(a(a(c(c(d(d(b(b(x0))))))))))))) → D(d(b(b(d(b(b(c(c(d(d(b(b(x0)))))))))))))
D(d(c(c(d(a(a(c(c(b(b(b(x0)))))))))))) → D(d(b(b(d(b(a(a(b(b(c(c(x0))))))))))))
D(d(c(c(d(a(a(c(c(b(b(b(b(b(x0)))))))))))))) → D(d(b(b(d(b(b(b(a(a(b(b(c(c(x0))))))))))))))
D(d(c(c(d(a(a(c(c(b(b(b(b(x0))))))))))))) → D(d(b(b(d(b(b(a(a(b(b(c(c(x0)))))))))))))

↳ QTRS

  ↳ QTRS Reverse

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

                ↳ QDP

                  ↳ RuleRemovalProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ QDP

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ DependencyGraphProof

              ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

D(d(c(c(d(a(a(c(c(d(d(b(b(x0))))))))))))) → D(d(b(b(d(b(b(c(c(d(d(b(b(x0)))))))))))))
D(d(c(c(d(a(a(c(c(b(d(d(b(b(x0)))))))))))))) → D(d(b(b(d(b(b(b(c(c(d(d(b(b(x0))))))))))))))
D(d(c(c(d(c(c(x0))))))) → D(d(b(b(d(b(b(d(d(x0)))))))))
D(d(c(c(d(c(c(x0))))))) → D(d(b(b(d(d(d(b(b(d(d(x0)))))))))))
D(d(c(c(d(a(a(c(c(b(b(b(b(b(x0)))))))))))))) → D(d(b(b(d(b(b(b(a(a(b(b(c(c(x0))))))))))))))
D(d(c(c(b(b(x0)))))) → D(d(c(c(d(d(b(b(x0))))))))
D(d(c(c(d(a(a(c(c(b(b(b(b(x0))))))))))))) → D(d(b(b(d(b(b(a(a(b(b(c(c(x0)))))))))))))
D(d(c(c(d(a(a(c(c(b(b(x0))))))))))) → D(d(b(b(d(a(a(b(b(c(c(x0)))))))))))
D(d(c(c(d(a(a(c(c(b(b(b(x0)))))))))))) → D(d(b(b(d(b(a(a(b(b(c(c(x0))))))))))))
D(d(c(c(c(c(x0)))))) → D(d(b(b(d(d(b(b(d(d(x0))))))))))
D(d(c(c(c(c(x0)))))) → D(d(b(b(b(b(d(d(x0))))))))

The TRS R consists of the following rules:

d(d(c(c(x1)))) → b(b(d(d(x1))))
d(d(c(c(x1)))) → d(d(b(b(d(d(x1))))))
d(d(a(a(c(c(x1)))))) → b(b(b(b(x1))))
b(b(d(d(b(b(x1)))))) → c(c(d(d(b(b(x1))))))
b(b(b(b(b(b(x1)))))) → a(a(b(b(c(c(x1))))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 6 less nodes.

↳ QTRS

  ↳ QTRS Reverse

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

                ↳ QDP

                  ↳ RuleRemovalProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ QDP

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ DependencyGraphProof

                                            ↳ QDP

                                              ↳ SemLabProof

                                              ↳ SemLabProof2

              ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

D(d(c(c(d(c(c(x0))))))) → D(d(b(b(d(b(b(d(d(x0)))))))))
D(d(c(c(d(c(c(x0))))))) → D(d(b(b(d(d(d(b(b(d(d(x0)))))))))))
D(d(c(c(b(b(x0)))))) → D(d(c(c(d(d(b(b(x0))))))))
D(d(c(c(c(c(x0)))))) → D(d(b(b(d(d(b(b(d(d(x0))))))))))
D(d(c(c(c(c(x0)))))) → D(d(b(b(b(b(d(d(x0))))))))

The TRS R consists of the following rules:

d(d(c(c(x1)))) → b(b(d(d(x1))))
d(d(c(c(x1)))) → d(d(b(b(d(d(x1))))))
d(d(a(a(c(c(x1)))))) → b(b(b(b(x1))))
b(b(d(d(b(b(x1)))))) → c(c(d(d(b(b(x1))))))
b(b(b(b(b(b(x1)))))) → a(a(b(b(c(c(x1))))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We found the following model for the rules of the TRS R. Interpretation over the domain with elements from 0 to 1.c: 0
D: 0
a: 0
b: 0
d: 1 + x₀
By semantic labelling [33] we obtain the following labelled TRS:Q DP problem:
The TRS P consists of the following rules:

D.1(d.0(c.0(c.1(d.0(c.0(c.0(x0))))))) → D.1(d.0(b.0(b.1(d.0(b.0(b.0(d.1(d.0(x0)))))))))
D.1(d.0(c.0(c.0(c.0(c.1(x0)))))) → D.1(d.0(b.0(b.0(d.1(d.0(b.0(b.1(d.0(d.1(x0))))))))))
D.1(d.0(c.0(c.0(b.0(b.1(x0)))))) → D.1(d.0(c.0(c.0(d.1(d.0(b.0(b.1(x0))))))))
D.1(d.0(c.0(c.0(c.0(c.0(x0)))))) → D.1(d.0(b.0(b.0(d.1(d.0(b.0(b.0(d.1(d.0(x0))))))))))
D.1(d.0(c.0(c.1(d.0(c.0(c.0(x0))))))) → D.1(d.0(b.0(b.1(d.0(d.1(d.0(b.0(b.0(d.1(d.0(x0)))))))))))
D.1(d.0(c.0(c.0(b.0(b.0(x0)))))) → D.1(d.0(c.0(c.0(d.1(d.0(b.0(b.0(x0))))))))
D.1(d.0(c.0(c.1(d.0(c.0(c.1(x0))))))) → D.1(d.0(b.0(b.1(d.0(d.1(d.0(b.0(b.1(d.0(d.1(x0)))))))))))
D.1(d.0(c.0(c.0(c.0(c.0(x0)))))) → D.1(d.0(b.0(b.0(b.0(b.0(d.1(d.0(x0))))))))
D.1(d.0(c.0(c.1(d.0(c.0(c.1(x0))))))) → D.1(d.0(b.0(b.1(d.0(b.0(b.1(d.0(d.1(x0)))))))))
D.1(d.0(c.0(c.0(c.0(c.1(x0)))))) → D.1(d.0(b.0(b.0(b.0(b.1(d.0(d.1(x0))))))))

The TRS R consists of the following rules:

b.0(b.0(b.0(b.0(b.0(b.0(x1)))))) → a.0(a.0(b.0(b.0(c.0(c.0(x1))))))
b.0(b.0(d.1(d.0(b.0(b.0(x1)))))) → c.0(c.0(d.1(d.0(b.0(b.0(x1))))))
d.1(d.0(a.0(a.0(c.0(c.0(x1)))))) → b.0(b.0(b.0(b.0(x1))))
d.1(d.0(c.0(c.1(x1)))) → b.0(b.1(d.0(d.1(x1))))
b.0(b.0(d.1(d.0(b.0(b.1(x1)))))) → c.0(c.0(d.1(d.0(b.0(b.1(x1))))))
d.1(d.0(a.0(a.0(c.0(c.1(x1)))))) → b.0(b.0(b.0(b.1(x1))))
d.1(d.0(c.0(c.1(x1)))) → d.1(d.0(b.0(b.1(d.0(d.1(x1))))))
d.1(d.0(c.0(c.0(x1)))) → b.0(b.0(d.1(d.0(x1))))
b.0(b.0(b.0(b.0(b.0(b.1(x1)))))) → a.0(a.0(b.0(b.0(c.0(c.1(x1))))))
d.1(d.0(c.0(c.0(x1)))) → d.1(d.0(b.0(b.0(d.1(d.0(x1))))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ QTRS Reverse

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

                ↳ QDP

                  ↳ RuleRemovalProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ QDP

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ DependencyGraphProof

                                            ↳ QDP

                                              ↳ SemLabProof

                                                ↳ QDP

                                                  ↳ DependencyGraphProof

                                              ↳ SemLabProof2

              ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

D.1(d.0(c.0(c.1(d.0(c.0(c.0(x0))))))) → D.1(d.0(b.0(b.1(d.0(b.0(b.0(d.1(d.0(x0)))))))))
D.1(d.0(c.0(c.0(c.0(c.1(x0)))))) → D.1(d.0(b.0(b.0(d.1(d.0(b.0(b.1(d.0(d.1(x0))))))))))
D.1(d.0(c.0(c.0(b.0(b.1(x0)))))) → D.1(d.0(c.0(c.0(d.1(d.0(b.0(b.1(x0))))))))
D.1(d.0(c.0(c.0(c.0(c.0(x0)))))) → D.1(d.0(b.0(b.0(d.1(d.0(b.0(b.0(d.1(d.0(x0))))))))))
D.1(d.0(c.0(c.1(d.0(c.0(c.0(x0))))))) → D.1(d.0(b.0(b.1(d.0(d.1(d.0(b.0(b.0(d.1(d.0(x0)))))))))))
D.1(d.0(c.0(c.0(b.0(b.0(x0)))))) → D.1(d.0(c.0(c.0(d.1(d.0(b.0(b.0(x0))))))))
D.1(d.0(c.0(c.1(d.0(c.0(c.1(x0))))))) → D.1(d.0(b.0(b.1(d.0(d.1(d.0(b.0(b.1(d.0(d.1(x0)))))))))))
D.1(d.0(c.0(c.0(c.0(c.0(x0)))))) → D.1(d.0(b.0(b.0(b.0(b.0(d.1(d.0(x0))))))))
D.1(d.0(c.0(c.1(d.0(c.0(c.1(x0))))))) → D.1(d.0(b.0(b.1(d.0(b.0(b.1(d.0(d.1(x0)))))))))
D.1(d.0(c.0(c.0(c.0(c.1(x0)))))) → D.1(d.0(b.0(b.0(b.0(b.1(d.0(d.1(x0))))))))

The TRS R consists of the following rules:

b.0(b.0(b.0(b.0(b.0(b.0(x1)))))) → a.0(a.0(b.0(b.0(c.0(c.0(x1))))))
b.0(b.0(d.1(d.0(b.0(b.0(x1)))))) → c.0(c.0(d.1(d.0(b.0(b.0(x1))))))
d.1(d.0(a.0(a.0(c.0(c.0(x1)))))) → b.0(b.0(b.0(b.0(x1))))
d.1(d.0(c.0(c.1(x1)))) → b.0(b.1(d.0(d.1(x1))))
b.0(b.0(d.1(d.0(b.0(b.1(x1)))))) → c.0(c.0(d.1(d.0(b.0(b.1(x1))))))
d.1(d.0(a.0(a.0(c.0(c.1(x1)))))) → b.0(b.0(b.0(b.1(x1))))
d.1(d.0(c.0(c.1(x1)))) → d.1(d.0(b.0(b.1(d.0(d.1(x1))))))
d.1(d.0(c.0(c.0(x1)))) → b.0(b.0(d.1(d.0(x1))))
b.0(b.0(b.0(b.0(b.0(b.1(x1)))))) → a.0(a.0(b.0(b.0(c.0(c.1(x1))))))
d.1(d.0(c.0(c.0(x1)))) → d.1(d.0(b.0(b.0(d.1(d.0(x1))))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 7 less nodes.

↳ QTRS

  ↳ QTRS Reverse

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

                ↳ QDP

                  ↳ RuleRemovalProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ QDP

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ DependencyGraphProof

                                            ↳ QDP

                                              ↳ SemLabProof

                                                ↳ QDP

                                                  ↳ DependencyGraphProof

                                                    ↳ QDP

                                              ↳ SemLabProof2

              ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

D.1(d.0(c.0(c.0(c.0(c.0(x0)))))) → D.1(d.0(b.0(b.0(d.1(d.0(b.0(b.0(d.1(d.0(x0))))))))))
D.1(d.0(c.0(c.0(b.0(b.0(x0)))))) → D.1(d.0(c.0(c.0(d.1(d.0(b.0(b.0(x0))))))))
D.1(d.0(c.0(c.0(c.0(c.0(x0)))))) → D.1(d.0(b.0(b.0(b.0(b.0(d.1(d.0(x0))))))))

The TRS R consists of the following rules:

b.0(b.0(b.0(b.0(b.0(b.0(x1)))))) → a.0(a.0(b.0(b.0(c.0(c.0(x1))))))
b.0(b.0(d.1(d.0(b.0(b.0(x1)))))) → c.0(c.0(d.1(d.0(b.0(b.0(x1))))))
d.1(d.0(a.0(a.0(c.0(c.0(x1)))))) → b.0(b.0(b.0(b.0(x1))))
d.1(d.0(c.0(c.1(x1)))) → b.0(b.1(d.0(d.1(x1))))
b.0(b.0(d.1(d.0(b.0(b.1(x1)))))) → c.0(c.0(d.1(d.0(b.0(b.1(x1))))))
d.1(d.0(a.0(a.0(c.0(c.1(x1)))))) → b.0(b.0(b.0(b.1(x1))))
d.1(d.0(c.0(c.1(x1)))) → d.1(d.0(b.0(b.1(d.0(d.1(x1))))))
d.1(d.0(c.0(c.0(x1)))) → b.0(b.0(d.1(d.0(x1))))
b.0(b.0(b.0(b.0(b.0(b.1(x1)))))) → a.0(a.0(b.0(b.0(c.0(c.1(x1))))))
d.1(d.0(c.0(c.0(x1)))) → d.1(d.0(b.0(b.0(d.1(d.0(x1))))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
As can be seen after transforming the QDP problem by semantic labelling [33] and then some rule deleting processors, only certain labelled rules and pairs can be used. Hence, we only have to consider all unlabelled pairs and rules (without the decreasing rules for quasi-models).

↳ QTRS

  ↳ QTRS Reverse

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

                ↳ QDP

                  ↳ RuleRemovalProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ QDP

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ DependencyGraphProof

                                            ↳ QDP

                                              ↳ SemLabProof

                                              ↳ SemLabProof2

                                                ↳ QDP

                                                  ↳ QDPToSRSProof

              ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

D(d(c(c(b(b(x0)))))) → D(d(c(c(d(d(b(b(x0))))))))
D(d(c(c(c(c(x0)))))) → D(d(b(b(d(d(b(b(d(d(x0))))))))))
D(d(c(c(c(c(x0)))))) → D(d(b(b(b(b(d(d(x0))))))))

The TRS R consists of the following rules:

d(d(c(c(x1)))) → b(b(d(d(x1))))
d(d(c(c(x1)))) → d(d(b(b(d(d(x1))))))
d(d(a(a(c(c(x1)))))) → b(b(b(b(x1))))
b(b(d(d(b(b(x1)))))) → c(c(d(d(b(b(x1))))))
b(b(b(b(b(b(x1)))))) → a(a(b(b(c(c(x1))))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The finiteness of this DP problem is implied by strong termination of a SRS due to [12].

↳ QTRS

  ↳ QTRS Reverse

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

                ↳ QDP

                  ↳ RuleRemovalProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ QDP

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ DependencyGraphProof

                                            ↳ QDP

                                              ↳ SemLabProof

                                              ↳ SemLabProof2

                                                ↳ QDP

                                                  ↳ QDPToSRSProof

                                                    ↳ QTRS

                                                      ↳ QTRS Reverse

              ↳ UsableRulesProof

Q restricted rewrite system:
The TRS R consists of the following rules:

d(d(c(c(x1)))) → b(b(d(d(x1))))
d(d(c(c(x1)))) → d(d(b(b(d(d(x1))))))
d(d(a(a(c(c(x1)))))) → b(b(b(b(x1))))
b(b(d(d(b(b(x1)))))) → c(c(d(d(b(b(x1))))))
b(b(b(b(b(b(x1)))))) → a(a(b(b(c(c(x1))))))
D(d(c(c(b(b(x0)))))) → D(d(c(c(d(d(b(b(x0))))))))
D(d(c(c(c(c(x0)))))) → D(d(b(b(d(d(b(b(d(d(x0))))))))))
D(d(c(c(c(c(x0)))))) → D(d(b(b(b(b(d(d(x0))))))))

Q is empty.

We have reversed the following QTRS:
The set of rules R is

d(d(c(c(x1)))) → b(b(d(d(x1))))
d(d(c(c(x1)))) → d(d(b(b(d(d(x1))))))
d(d(a(a(c(c(x1)))))) → b(b(b(b(x1))))
b(b(d(d(b(b(x1)))))) → c(c(d(d(b(b(x1))))))
b(b(b(b(b(b(x1)))))) → a(a(b(b(c(c(x1))))))
D(d(c(c(b(b(x0)))))) → D(d(c(c(d(d(b(b(x0))))))))
D(d(c(c(c(c(x0)))))) → D(d(b(b(d(d(b(b(d(d(x0))))))))))
D(d(c(c(c(c(x0)))))) → D(d(b(b(b(b(d(d(x0))))))))

The set Q is empty.
We have obtained the following QTRS:

c(c(d(d(x)))) → d(d(b(b(x))))
c(c(d(d(x)))) → d(d(b(b(d(d(x))))))
c(c(a(a(d(d(x)))))) → b(b(b(b(x))))
b(b(d(d(b(b(x)))))) → b(b(d(d(c(c(x))))))
b(b(b(b(b(b(x)))))) → c(c(b(b(a(a(x))))))
b(b(c(c(d(D(x)))))) → b(b(d(d(c(c(d(D(x))))))))
c(c(c(c(d(D(x)))))) → d(d(b(b(d(d(b(b(d(D(x))))))))))
c(c(c(c(d(D(x)))))) → d(d(b(b(b(b(d(D(x))))))))

The set Q is empty.

↳ QTRS

  ↳ QTRS Reverse

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

                ↳ QDP

                  ↳ RuleRemovalProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ QDP

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ DependencyGraphProof

                                            ↳ QDP

                                              ↳ SemLabProof

                                              ↳ SemLabProof2

                                                ↳ QDP

                                                  ↳ QDPToSRSProof

                                                    ↳ QTRS

                                                      ↳ QTRS Reverse

                                                        ↳ QTRS

                                                          ↳ RFCMatchBoundsTRSProof

              ↳ UsableRulesProof

Q restricted rewrite system:
The TRS R consists of the following rules:

c(c(d(d(x)))) → d(d(b(b(x))))
c(c(d(d(x)))) → d(d(b(b(d(d(x))))))
c(c(a(a(d(d(x)))))) → b(b(b(b(x))))
b(b(d(d(b(b(x)))))) → b(b(d(d(c(c(x))))))
b(b(b(b(b(b(x)))))) → c(c(b(b(a(a(x))))))
b(b(c(c(d(D(x)))))) → b(b(d(d(c(c(d(D(x))))))))
c(c(c(c(d(D(x)))))) → d(d(b(b(d(d(b(b(d(D(x))))))))))
c(c(c(c(d(D(x)))))) → d(d(b(b(b(b(d(D(x))))))))

Q is empty.

Termination of the TRS R could be shown with a Match Bound [6,7] of 2. This implies Q-termination of R.
The following rules were used to construct the certificate:

c(c(d(d(x)))) → d(d(b(b(x))))
c(c(d(d(x)))) → d(d(b(b(d(d(x))))))
c(c(a(a(d(d(x)))))) → b(b(b(b(x))))
b(b(d(d(b(b(x)))))) → b(b(d(d(c(c(x))))))
b(b(b(b(b(b(x)))))) → c(c(b(b(a(a(x))))))
b(b(c(c(d(D(x)))))) → b(b(d(d(c(c(d(D(x))))))))
c(c(c(c(d(D(x)))))) → d(d(b(b(d(d(b(b(d(D(x))))))))))
c(c(c(c(d(D(x)))))) → d(d(b(b(b(b(d(D(x))))))))

The certificate found is represented by the following graph.

The certificate consists of the following enumerated nodes:

5680, 5681, 5686, 5685, 5684, 5683, 5682, 5693, 5694, 5692, 5689, 5690, 5688, 5695, 5691, 5687, 5696, 5697, 5698, 5699, 5700, 5705, 5706, 5704, 5703, 5702, 5707, 5701, 5708, 5709, 5714, 5713, 5710, 5711, 5712, 5717, 5716, 5715, 5722, 5721, 5720, 5719, 5718, 5723, 5724, 5725, 5726, 5727, 5728, 5729, 5734, 5733, 5730, 5731, 5732, 5741, 5742, 5740, 5737, 5738, 5736, 5743, 5739, 5735, 5751, 5752, 5750, 5749, 5748, 5753, 5747, 5756, 5755, 5754, 5762, 5763, 5766, 5765, 5764, 5767, 5768, 5769, 5770, 5771, 5772, 5773, 5776, 5775, 5774

Node 5680 is start node and node 5681 is final node.

Those nodes are connect through the following edges:

5680 to 5682 labelled c_1(0)
5680 to 5687 labelled d_1(0)
5680 to 5696 labelled b_1(0)
5680 to 5701 labelled d_1(0)
5680 to 5708 labelled b_1(0)
5680 to 5715 labelled b_1(0)
5680 to 5718 labelled c_1(1)
5680 to 5767 labelled b_1(1)
5681 to 5681 labelled #_1(0)
5686 to 5681 labelled a_1(0)
5685 to 5686 labelled a_1(0)
5684 to 5685 labelled b_1(0)
5683 to 5684 labelled b_1(0)
5682 to 5683 labelled c_1(0)
5693 to 5694 labelled b_1(0)
5694 to 5695 labelled d_1(0)
5692 to 5693 labelled b_1(0)
5689 to 5690 labelled b_1(0)
5689 to 5681 labelled b_1(0)
5689 to 5718 labelled c_1(1)
5689 to 5723 labelled b_1(1)
5689 to 5728 labelled b_1(1)
5689 to 5772 labelled b_1(2)
5690 to 5691 labelled d_1(0)
5688 to 5689 labelled b_1(0)
5688 to 5718 labelled c_1(1)
5688 to 5723 labelled b_1(1)
5688 to 5728 labelled b_1(1)
5688 to 5772 labelled b_1(2)
5695 to 5681 labelled D_1(0)
5691 to 5692 labelled d_1(0)
5691 to 5681 labelled d_1(0)
5687 to 5688 labelled d_1(0)
5696 to 5697 labelled b_1(0)
5697 to 5698 labelled d_1(0)
5698 to 5699 labelled d_1(0)
5699 to 5700 labelled c_1(0)
5699 to 5735 labelled d_1(1)
5699 to 5747 labelled d_1(1)
5699 to 5754 labelled b_1(1)
5699 to 5718 labelled c_1(1)
5700 to 5681 labelled c_1(0)
5700 to 5735 labelled d_1(1)
5700 to 5747 labelled d_1(1)
5700 to 5754 labelled b_1(1)
5700 to 5718 labelled c_1(1)
5705 to 5706 labelled b_1(0)
5706 to 5707 labelled d_1(0)
5704 to 5705 labelled b_1(0)
5703 to 5704 labelled b_1(0)
5702 to 5703 labelled b_1(0)
5707 to 5681 labelled D_1(0)
5701 to 5702 labelled d_1(0)
5708 to 5709 labelled b_1(0)
5709 to 5710 labelled d_1(0)
5714 to 5681 labelled D_1(0)
5713 to 5714 labelled d_1(0)
5710 to 5711 labelled d_1(0)
5711 to 5712 labelled c_1(0)
5712 to 5713 labelled c_1(0)
5717 to 5681 labelled b_1(0)
5717 to 5718 labelled c_1(1)
5717 to 5723 labelled b_1(1)
5717 to 5728 labelled b_1(1)
5717 to 5772 labelled b_1(2)
5716 to 5717 labelled b_1(0)
5716 to 5718 labelled c_1(1)
5716 to 5723 labelled b_1(1)
5716 to 5728 labelled b_1(1)
5716 to 5772 labelled b_1(2)
5715 to 5716 labelled b_1(0)
5715 to 5718 labelled c_1(1)
5722 to 5681 labelled a_1(1)
5721 to 5722 labelled a_1(1)
5720 to 5721 labelled b_1(1)
5719 to 5720 labelled b_1(1)
5718 to 5719 labelled c_1(1)
5723 to 5724 labelled b_1(1)
5724 to 5725 labelled d_1(1)
5725 to 5726 labelled d_1(1)
5726 to 5727 labelled c_1(1)
5726 to 5735 labelled d_1(1)
5726 to 5747 labelled d_1(1)
5726 to 5754 labelled b_1(1)
5726 to 5718 labelled c_1(1)
5727 to 5681 labelled c_1(1)
5727 to 5694 labelled c_1(1)
5727 to 5735 labelled d_1(1)
5727 to 5747 labelled d_1(1)
5727 to 5754 labelled b_1(1)
5727 to 5718 labelled c_1(1)
5728 to 5729 labelled b_1(1)
5729 to 5730 labelled d_1(1)
5734 to 5681 labelled D_1(1)
5733 to 5734 labelled d_1(1)
5730 to 5731 labelled d_1(1)
5731 to 5732 labelled c_1(1)
5732 to 5733 labelled c_1(1)
5741 to 5742 labelled b_1(1)
5742 to 5743 labelled d_1(1)
5740 to 5741 labelled b_1(1)
5737 to 5738 labelled b_1(1)
5737 to 5681 labelled b_1(1)
5737 to 5718 labelled c_1(1)
5737 to 5723 labelled b_1(1)
5737 to 5728 labelled b_1(1)
5737 to 5772 labelled b_1(2)
5738 to 5739 labelled d_1(1)
5736 to 5737 labelled b_1(1)
5736 to 5718 labelled c_1(1)
5736 to 5723 labelled b_1(1)
5736 to 5728 labelled b_1(1)
5736 to 5762 labelled b_1(2)
5736 to 5772 labelled b_1(2)
5743 to 5681 labelled D_1(1)
5739 to 5740 labelled d_1(1)
5739 to 5681 labelled d_1(1)
5735 to 5736 labelled d_1(1)
5751 to 5752 labelled b_1(1)
5752 to 5753 labelled d_1(1)
5750 to 5751 labelled b_1(1)
5749 to 5750 labelled b_1(1)
5748 to 5749 labelled b_1(1)
5753 to 5681 labelled D_1(1)
5747 to 5748 labelled d_1(1)
5756 to 5681 labelled b_1(1)
5756 to 5718 labelled c_1(1)
5756 to 5723 labelled b_1(1)
5756 to 5728 labelled b_1(1)
5756 to 5772 labelled b_1(2)
5755 to 5756 labelled b_1(1)
5755 to 5718 labelled c_1(1)
5755 to 5723 labelled b_1(1)
5755 to 5728 labelled b_1(1)
5755 to 5772 labelled b_1(2)
5754 to 5755 labelled b_1(1)
5754 to 5718 labelled c_1(1)
5762 to 5763 labelled b_1(2)
5763 to 5764 labelled d_1(2)
5766 to 5742 labelled c_1(2)
5765 to 5766 labelled c_1(2)
5764 to 5765 labelled d_1(2)
5767 to 5768 labelled b_1(1)
5768 to 5769 labelled d_1(1)
5769 to 5770 labelled d_1(1)
5770 to 5771 labelled c_1(1)
5771 to 5755 labelled c_1(1)
5772 to 5773 labelled b_1(2)
5773 to 5774 labelled d_1(2)
5776 to 5755 labelled c_1(2)
5775 to 5776 labelled c_1(2)
5774 to 5775 labelled d_1(2)

We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS

  ↳ QTRS Reverse

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

              ↳ UsableRulesProof

                ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

D(d(c(c(x1)))) → D(d(x1))
D(d(c(c(x1)))) → D(b(b(d(d(x1)))))
D(d(c(c(x1)))) → D(d(b(b(d(d(x1))))))
D(d(c(c(x1)))) → D(x1)

The TRS R consists of the following rules:

d(d(c(c(x1)))) → b(b(d(d(x1))))
d(d(c(c(x1)))) → d(d(b(b(d(d(x1))))))
d(d(a(a(c(c(x1)))))) → b(b(b(b(x1))))
b(b(d(d(b(b(x1)))))) → c(c(d(d(b(b(x1))))))
b(b(b(b(b(b(x1)))))) → a(a(b(b(c(c(x1))))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.